The development of complex high-assurance hardware platforms for commercial and military control systems, such as avionics and communications, and secure computing applications such as crypto modernization, guard applications and Multiple Independent Levels of Security (MILS) separation has generated a need for an efficient development and certification path for such high-assurance computing elements. To date, traditional approaches to the development and verification of computational elements, such as microprocessors, have been labor intensive, error prone, and have lacked a formal specification for their implementation.
Design elements have been based on textual specifications and implemented with hand-coded hardware description languages (HDL) such as VHDL and Verilog. Verification has been performed through simulations which are driven by hand-generated test cases, corner case stimulus, or random input stimulus.
To develop and certify high-assurance devices, traditional approaches are inadequate due to the possibility of errors in specification interpretation, hand coding and incomplete test case coverage. In addition, the artifacts and proofs of correctness necessary for the rigorous nature of high-assurance certification are not inherent to the process and must be generated at the end of the design cycle.
As such, there is a need for efficient methods and systems for the design of high-assurance computing elements which integrate current model-based design principles with automatic code generation of higher order language (HOL) computer code and associated test cases, and automated analysis tools, such as model checkers and theorem provers. Such methods and systems provide designs having a documented pedigree of correctness.